open import Data.Nat
open import Data.Vec
open import Relation.Binary.Core
open import Algebra.Structures
open import Algebra
open import Agda.Builtin.Unit
open import Data.Empty
open import Relation.Nullary
--open import Data.Nat renaming (_⊔_ to _ℕ⊔_ ; _+_ to _ℕ+_)
open import Data.Product
--open import Data.Nat.Properties 
open import Data.Bool renaming ( _≟_ to _B≟_)
open import Agda.Builtin.Equality
open import Data.Integer renaming (_*_ to _ℤ*_ ; _+_ to _ℤ+_)
open import Data.Integer.Properties
open import Agda.Builtin.Equality
open import Data.Empty
--    dec = _≟_
--    polyType = UnivariatePolyOverCommutativeRing +-*-commutativeRing dec

module UnivariatePolynomialTest where
open import UnivariatePolynomial  +-*-commutativeRing Data.Integer._≟_


q = (+ 2) ∷ (Data.Integer.- (+ 3)) ∷ (+ 20) ∷ []
q' = (Data.Integer.- (+ 2)) ∷ (Data.Integer.- (+ 3)) ∷ (+ 20) ∷ []
w = (+ 1)  ∷ (+ 10) ∷ []
w' = (+ 4)  ∷ (+ 10) ∷ []
w'' = (+ 5)  ∷ (+ 10) ∷ []

e = addPolys q w
qq : (proj₁ (proj₂ (proj₂ e))) ≡  + 2 ∷ (- (+ 2)) ∷ + 30 ∷ []
qq = refl

qq2 : (proj₁ (proj₂ (proj₂ (addPolys w q)))) ≡  + 2 ∷ (- (+ 2)) ∷ + 30 ∷ []
qq2 = refl


qq3 : (proj₁ (proj₂ (proj₂ (addPolys q' q)))) ≡   (- (+ 6)) ∷ + 40 ∷ []
qq3 = refl


qq4 : (proj₁ (proj₂ (proj₂ (multiplyByX q)))) ≡   (+ 2) ∷ (Data.Integer.- (+ 3)) ∷ (+ 20) ∷ (+ 0) ∷ []
qq4 = refl
qq4' : (proj₁ (proj₂ (proj₂ (multiplyByX [])))) ≡ []
qq4' = refl
qq4'' : (proj₁ (proj₂ (proj₂ (multiplyByX [(+ 1)])))) ≡ (+ 1) ∷ (+ 0) ∷ []
qq4'' = refl
qq5 : (proj₁ (proj₂ (proj₂ (multiplyByScalar q (+ 2))))) ≡   (+ 4) ∷ (Data.Integer.- (+ 6)) ∷ (+ 40) ∷  []
qq5 = refl

qq6 : (proj₁ (proj₂ (proj₂ (multiplyPolys q  ( (+ 1) ∷ []))))) ≡  q
qq6 = refl

qq7 : (proj₁ (proj₂ (proj₂ (multiplyPolys ( (+ 1) ∷ []) q)))) ≡  q
qq7 = refl


qq6p : (proj₁ (proj₂ (proj₂ (multiplyPolys q  (  []))))) ≡  []
qq6p = refl
qq7p : (proj₁ (proj₂ (proj₂ (multiplyPolys (  []) q)))) ≡  []
qq7p = refl

qq6z : (proj₁ (proj₂ (proj₂ (multiplyPolys q  ( (+ 5) ∷ []))))) ≡  (proj₁ (proj₂ (proj₂ (multiplyByScalar q (+ 5)))))
qq6z = refl
qq7z : (proj₁ (proj₂ (proj₂ (multiplyPolys ( (+ 5) ∷ []) q)))) ≡  (proj₁ (proj₂ (proj₂ (multiplyByScalar q (+ 5)))))
qq7z = refl


{--
(2x2 -3x 20) * (4x 10)
 w'' 5 10
--}
eeee = (+ 8) ∷ (+ 8) ∷ (+ 50) ∷ (+ 200) ∷ []
qq6z1 : (proj₁ (proj₂ (proj₂ (multiplyPolys q  w')))) ≡  eeee
qq6z1 = refl
qq7z1 : (proj₁ (proj₂ (proj₂ (multiplyPolys w' q)))) ≡  eeee
qq7z1 = refl

eeee′ = (+ 10) ∷ (+ 5) ∷ (+ 70) ∷ (+ 200) ∷ []
qq6z1' : (proj₁ (proj₂ (proj₂ (multiplyPolys q  w'')))) ≡  eeee′
qq6z1' = refl
qq7z1' : (proj₁ (proj₂ (proj₂ (multiplyPolys w'' q)))) ≡  eeee′
qq7z1' = refl

q2 = (Data.Integer.- (+ 10)) ∷ (+ 300) ∷ (+ 1) ∷ (+ 100) ∷ []


~_  = Data.Integer.-_
eeee′2 = (~ (+ 20)) ∷ + 630 ∷ (~ (+ 1098))   ∷ + 6197 ∷ ~ (+ 280) ∷ + 2000 ∷ []
qq6z1'q : (proj₁ (proj₂ (proj₂ (multiplyPolys q  q2)))) ≡  eeee′2
qq6z1'q = refl
qq7z1'q : (proj₁ (proj₂ (proj₂ (multiplyPolys q2 q)))) ≡  eeee′2
qq7z1'q = refl
qq7z1'q≡ : (multiplyPolys q2 q) ≡ (multiplyPolys q q2)
qq7z1'q≡ = refl


p0 : coeffOfPower 0 eeee′2 ≡ (+ 2000)
p0 = refl
p2 : coeffOfPower 1 eeee′2 ≡ ~ (+  280)
p2 = refl
p5 : coeffOfPower 5 eeee′2 ≡ ~ (+  20)
p5 = refl
p6 : coeffOfPower 6 eeee′2 ≡ ~ (+  0)
p6 = refl
p7 : coeffOfPower 7 eeee′2 ≡ ~ (+  0)
p7 = refl
